Nuprl Lemma : uni_sat_imp_in_uni_set
2,24
postcript
pdf
T
:Type,
a
:
T
,
Q
:(
T
Prop). (
a
=!
x
:
T
.
Q
(
x
))
a
{!
x
:
T
|
Q
(
x
)}
latex
Definitions
a
=!
x
:
T
.
Q
(
x
)
,
{!
x
:
T
|
P
(
x
)}
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s
)
,
Prop
,
t
T
origin
T:Type, a:T, Q:(T
Prop). (a =!x:T. Q(x)) 
a 
{!x:T | Q(x)} T:Type, a:T, Q:(TProp). (a =!x:T. Q(x)) a {!x:T | Q(x)} x:A. B(x) Q T